#include "cuddObj.hh"
#include "formula.hh"
#include "utilities.hh"
#include <sstream>

using namespace std;






// Constructors
Formula::Formula (string n) {
  op = 0;
  name = n;
  EC = new vector<BDD *>();
}

Formula::Formula(unsigned short int o, Formula *f1) {
  op = o;
  left = f1;
  EC = new vector<BDD *>();
}

Formula::Formula(unsigned short int o, Formula *f1, Formula *f2) {
  op = o;
  left = f1;
  right = f2;
  EC = new vector<BDD *>();
}


// Setters
void Formula::set_depth(unsigned short int d) {
  depth = d;
}

void Formula::set_model_depth(unsigned int d) {
  model_depth = d;
}

void Formula::set_EC(vector<BDD *> *EqCl) {
  (*EC) = (*EqCl);    
}

void Formula::set_name(string n) {
  name =n;
}

// Getters
unsigned short int Formula::get_op() { return op; }

string Formula::get_name() { return name; }

Formula* Formula::get_left() { return left; }

Formula* Formula::get_right() { return right; }

unsigned short int Formula::get_depth() { return depth; }

unsigned int Formula::get_model_depth() { return model_depth; }

vector<BDD *>* Formula::get_EC() {
  return EC;
}

// Everything else
string Formula::to_string() {
  if (op==0) { 
    return name; 
  }
  else if (op==1) {
    return "("+left->to_string()+" AND "+ right->to_string()+")";
  }
  else if (op==2) {
    return "("+left->to_string()+" OR "+ right->to_string()+")";
  }
  else if (op==3) {
    return "NOT ("+left->to_string()+")";
  }
  else if (op==4) {
    return "("+left->to_string() + " -> " + right->to_string()+")";
  }
  else if (op==10) {
    return "(AG " + left->to_string()+")";
  }
  else if (op==11) {
    return "(EG " +left->to_string()+")";
  }
  else if (op==12) {
    return "(AX " + left->to_string()+")";
  }
  else if (op==13) {
    return "(EX " + left->to_string()+")";
  }
  else if (op==14) {
    return "(AF " + left->to_string()+")";
  }
  else if (op==15) {
    return "(EF " + left->to_string()+")";
  }
  else if (op==16) {
    return "A["+left->to_string() + " U " + right->to_string()+"]";
  }
  else if (op==17) {
    return "E["+left->to_string() + " U " + right->to_string()+"]";
  }
  else if (op==30) {
    return "K("+get_name()+", "+left->to_string()+")";
  }
  else if (op==31) {
    return "KPR("+get_name()+", "+left->to_string()+")";
  }
  else if (op==32) {
    std::string s;
    std::stringstream out;
    out << get_depth();
    s = out.str();
    return "KD(" + get_name() + ", depth=" + s
      + ", " + left->to_string() + ")";
  } else {
    return "UNKNOWN OPERATOR!";
  }
} // end Formula::to_string();


BDD* Formula::check_formula(BDDvector *v, BDDvector *pv, BDD *Rt, 
			    BDD *Ri, Cudd *bddmgr,   
			    map<string, BDD*> *evaluation,
                            BDD *reach) {

  // TODO: implement temporal operators
  BDD *result = new BDD(bddmgr->bddZero());

  if ( op == 0 ) { // term
    // TODO: check that proposition is in evaluation
    result = (*evaluation)[get_name()];
  }
  else if ( op == 1 ) { // and
    (*result) = *left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach)
      * *right->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach);
  }
  else if ( op == 2 ) { // or
    (*result) = *left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach)
      + *right->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach);
  }
  else if ( op == 3 ) { // not
    (*result) = (!(*left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach)))
                *(*reach);
  }
  else if ( op == 4 ) { // implies
    (*result) = ((!(*left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach)))
                  *(*reach))
      + *right->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,reach);
  }
  // TODO: introduce all temporal operators!
  else if ( op == 30 ) { // K
    
    BDD *tmp = new BDD(!(*left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
                         reach)));
    (*result) = (!(*check_nK(tmp,Ri,v,pv,bddmgr,reach)))*(*reach);
    
  }
  else if ( op == 31 ) { // KPR (perfect recall)
    
    BDD *tmp = new BDD((*left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
					     reach)));
    (*result) = (*Kn(model_depth,tmp,Rt,Ri,v,pv,EC,bddmgr,reach))*(*reach);
    
  }
  else if ( op == 32 ) { // KD, bounded recall
    
    BDD *tmp = new BDD((*left->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
                         reach)));
    (*result) = (*Kn(depth,tmp,Rt,Ri,v,pv,EC,bddmgr,reach))*(*reach);
    
  }

  (*result) = (*result) * (*reach);
  return result;

}
